\begin{tabbing}
$\forall$${\it the\_es}$:event\_system\{i:l\}. 
\\[0ex]trans(es{-}E(${\it the\_es}$); $e$,${\it e'}$.es{-}locl(${\it the\_es}$; $e$; ${\it e'}$))
\\[0ex]$\wedge$ SWellFounded(es{-}locl(${\it the\_es}$; $e$; ${\it e'}$))
\\[0ex]$\wedge$ \=($\forall$$e$,${\it e'}$:es{-}E(${\it the\_es}$).\+
\\[0ex](loc($e$) = loc(${\it e'}$) $\in$ Id)
\\[0ex]$\Leftarrow\!\Rightarrow$ (es{-}locl(${\it the\_es}$; $e$; ${\it e'}$) $\vee$ ($e$ = ${\it e'}$) $\vee$ es{-}locl(${\it the\_es}$; ${\it e'}$; $e$)))
\-\\[0ex]$\wedge$ \=($\forall$$e$:es{-}E(${\it the\_es}$). \+
\\[0ex]($\uparrow$es{-}first(${\it the\_es}$; $e$)) $\Leftarrow\!\Rightarrow$ ($\forall$${\it e'}$:es{-}E(${\it the\_es}$). $\neg$es{-}locl(${\it the\_es}$; ${\it e'}$; $e$)))
\-\\[0ex]$\wedge$ \=($\forall$$e$:es{-}E(${\it the\_es}$). \+
\\[0ex]($\neg$($\uparrow$es{-}first(${\it the\_es}$; $e$)))
\\[0ex]$\Rightarrow$ \=(es{-}locl(${\it the\_es}$; es{-}pred(${\it the\_es}$; $e$); $e$)\+
\\[0ex]$\wedge$ \=($\forall$${\it e'}$:es{-}E(${\it the\_es}$). \+
\\[0ex]$\neg$(es{-}locl(${\it the\_es}$; es{-}pred(${\it the\_es}$; $e$); ${\it e'}$) $\wedge$ es{-}locl(${\it the\_es}$; ${\it e'}$; $e$)))))
\-\-\-\\[0ex]$\wedge$ \=($\forall$$e$:es{-}E(${\it the\_es}$). \+
\\[0ex]($\neg$($\uparrow$es{-}first(${\it the\_es}$; $e$)))
\\[0ex]$\Rightarrow$ \=($\forall$$x$:Id, $t$:rationals.\+
\\[0ex]es\_state\_when(${\it the\_es}$; $e$)($x$,$t$)
\\[0ex]=
\\[0ex]es\_state\_after(${\it the\_es}$; es{-}pred(${\it the\_es}$; $e$))
\\[0ex]($x$
\\[0ex],$t$ + (es{-}time(${\it the\_es}$; $e$) {-} es{-}time(${\it the\_es}$; es{-}pred(${\it the\_es}$; $e$))))
\\[0ex]$\in$ es{-}vartype(${\it the\_es}$; loc($e$); $x$)))
\-\-\\[0ex]$\wedge$ trans(es{-}E(${\it the\_es}$); $e$,${\it e'}$.es{-}causl(${\it the\_es}$; $e$; ${\it e'}$))
\\[0ex]$\wedge$ SWellFounded(es{-}causl(${\it the\_es}$; $e$; ${\it e'}$))
\\[0ex]$\wedge$ \=($\forall$$e$:es{-}E(${\it the\_es}$). \+
\\[0ex]($\uparrow$es{-}isrcv(${\it the\_es}$; $e$))
\\[0ex]$\Rightarrow$ (\=es{-}sends(${\it the\_es}$; es{-}lnk(${\it the\_es}$; $e$); es{-}sender(${\it the\_es}$; $e$))[es{-}index(${\it the\_es}$; $e$)]\+
\\[0ex]=
\\[0ex]msg(es{-}lnk(${\it the\_es}$; $e$); es{-}tag(${\it the\_es}$; $e$); es{-}val(${\it the\_es}$; $e$))
\\[0ex]$\in$ es{-}Msg(${\it the\_es}$)))
\-\-\\[0ex]$\wedge$ ($\forall$$e$,${\it e'}$:es{-}E(${\it the\_es}$). es{-}locl(${\it the\_es}$; $e$; ${\it e'}$) $\Rightarrow$ es{-}causl(${\it the\_es}$; $e$; ${\it e'}$))
\\[0ex]$\wedge$ ($\forall$$e$:es{-}E(${\it the\_es}$). ($\uparrow$es{-}isrcv(${\it the\_es}$; $e$)) $\Rightarrow$ es{-}causl(${\it the\_es}$; es{-}sender(${\it the\_es}$; $e$); $e$))
\\[0ex]$\wedge$ \=($\forall$$e$,${\it e'}$:es{-}E(${\it the\_es}$).\+
\\[0ex]es{-}causl(${\it the\_es}$; $e$; ${\it e'}$)
\\[0ex]$\Rightarrow$ \=((($\neg$($\uparrow$es{-}first(${\it the\_es}$; ${\it e'}$)))\+
\\[0ex]c$\wedge$ (es{-}causl(${\it the\_es}$; $e$; es{-}pred(${\it the\_es}$; ${\it e'}$)) $\vee$ ($e$ = es{-}pred(${\it the\_es}$; ${\it e'}$))))
\\[0ex]$\vee$ \=(($\uparrow$es{-}isrcv(${\it the\_es}$; ${\it e'}$))\+
\\[0ex]c$\wedge$ (es{-}causl(${\it the\_es}$; $e$; es{-}sender(${\it the\_es}$; ${\it e'}$)) $\vee$ ($e$ = es{-}sender(${\it the\_es}$; ${\it e'}$))))))
\-\-\-\\[0ex]$\wedge$ \=($\forall$$e$:es{-}E(${\it the\_es}$). \+
\\[0ex]($\uparrow$es{-}isrcv(${\it the\_es}$; $e$)) $\Rightarrow$ (loc($e$) = destination(es{-}lnk(${\it the\_es}$; $e$)) $\in$ Id))
\-\\[0ex]$\wedge$ \=($\forall$$e$:es{-}E(${\it the\_es}$), $l$:IdLnk.\+
\\[0ex]($\neg$(loc($e$) = source($l$) $\in$ Id))
\\[0ex]$\Rightarrow$ (es{-}sends(${\it the\_es}$; $l$; $e$) = [] $\in$ (es{-}Msgl(${\it the\_es}$; $l$) List)))
\-\\[0ex]$\wedge$ \=($\forall$$e$,${\it e'}$:es{-}E(${\it the\_es}$).\+
\\[0ex]($\uparrow$es{-}isrcv(${\it the\_es}$; $e$))
\\[0ex]$\Rightarrow$ ($\uparrow$es{-}isrcv(${\it the\_es}$; ${\it e'}$))
\\[0ex]$\Rightarrow$ (es{-}lnk(${\it the\_es}$; $e$) = es{-}lnk(${\it the\_es}$; ${\it e'}$) $\in$ IdLnk)
\\[0ex]$\Rightarrow$ \=(es{-}locl(${\it the\_es}$; $e$; ${\it e'}$)\+
\\[0ex]$\Leftarrow\!\Rightarrow$ \=(es{-}locl(${\it the\_es}$; es{-}sender(${\it the\_es}$; $e$); es{-}sender(${\it the\_es}$; ${\it e'}$))\+
\\[0ex]$\vee$ \=((es{-}sender(${\it the\_es}$; $e$) = es{-}sender(${\it the\_es}$; ${\it e'}$) $\in$ es{-}E(${\it the\_es}$))\+
\\[0ex]$\wedge$ (es{-}index(${\it the\_es}$; $e$) $<$ es{-}index(${\it the\_es}$; ${\it e'}$))))))
\-\-\-\-\\[0ex]$\wedge$ \=($\forall$$e$:es{-}E(${\it the\_es}$), $l$:IdLnk, $n$:int\_seg(0; $\parallel$es{-}sends(${\it the\_es}$; $l$; $e$)$\parallel$).\+
\\[0ex]$\exists$\=${\it e'}$:es{-}E(${\it the\_es}$)\+
\\[0ex](($\uparrow$es{-}isrcv(${\it the\_es}$; ${\it e'}$))
\\[0ex]c$\wedge$ \=((es{-}lnk(${\it the\_es}$; ${\it e'}$) = $l$)\+
\\[0ex]$\wedge$ (es{-}sender(${\it the\_es}$; ${\it e'}$) = $e$)
\\[0ex]$\wedge$ (es{-}index(${\it the\_es}$; ${\it e'}$) = $n$ $\in$ $\mathbb{Z}$))))
\-\-\-
\end{tabbing}